;   The first S-expression in a MACLISP init file is a means of specifying
;   storage allocation, but we specify storage for the theorem-prover with a
;   call to MAKE-THM, which is defined in the file MAKE-THM.LISP.

(COMMENT)

;   TOPS-20 MACLISP has its own "device" mechanism.  If a symbol has a PPN
;   property, then the value of that property is used as the interpretation of
;   a device/directory specification that contains only one member.  For
;   example, if FOO has the PPN (A B), then (PROBEF '((FOO) X Y)) will
;   determine if there is a file A:<B>X.Y.  Loading the theorem-prover using
;   MAKE-THM depends upon the correct definition of the device THM.  Executing
;   the theorem prover, and even loading it, depend upn the corect definition
;   of the device LISP.  We mention this in detail because we have never seen
;   it documented.  At UTEXAS-20.ARPA, MACLISP is on PS:<MACLISP> and THM is on
;   AUX:<CL.THM>.  The next two lines may need modification elsewhere.

(PUTPROP (QUOTE LISP) (QUOTE (PS MACLISP)) (QUOTE PPN))
(PUTPROP (QUOTE THM) (QUOTE (AUX |CL.THM|)) (QUOTE PPN))
(PUTPROP (QUOTE  MAKE-THM) (QUOTE  ((THM) MAKE-THM FASL)) (QUOTE  AUTOLOAD))

;   Count with all the fingers.

(SETQ BASE 10. IBASE 10.)

;   None of the rest of this file is required to build a version of THM, but we
;   find it all valuable.

;  Permit deleting on display terminals even if the operating system does not
;  support VTS.

(SSTATUS LINMODE T)

;   Default to the currently connected directory rather than the PS equivalent.

(SETQ DEFAULTF (QUOTE ((*) FOO LSP)))

;  A debugger and a structure editor.

(FASLOAD FIXIT FASL LISP)

(PROG (FASLOAD) (FASLOAD UCEDIT FASL LISP))

;   To overcome not having loaded SLURP.FASL.

(DEFUN TYPE FEXPR (X)
  (PRINC (QUOTE |Type this file:  |) T)
  (PRIN1 X T)
  (TERPRI T))

;   An EMACS interface and dribble file startup.

(FASLOAD TOPS-20-EMACS-TO-THM FASL THM)